Inference at * 1 
Iof proof for Lemma bool ind:



1. P : 
2. P(ff)
3. P(tt)
4. b : 
  P(b) 

latex

 by ((BoolInd 4) 
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 4:n
C)) (first_tok :t) inil_term))) 

latex

C.

Definitions

t  T, Unit, , , tt, ff